The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
We consider the relative strengths of three formal approaches to public knowledge: “any fool” knowledge by McCarthy (1970), Common Knowledge by Halpern and Moses (1990), and Justified Knowledge by Artemov (2004). Specifically, we show that epistemic systems with the Common Knowledge modality C are conservative with respect to Justified Knowledge systems on formulas χ ∧ Cϕ→ψ, where χ, ϕ, and ψ are...
We introduce a natural deduction formulation for the Logic of Proofs, a refinement of modal logic S4 in which the assertion □ A is replaced by [[s]]A whose intended reading is “s is a proof of A”. A term calculus for this formulation yields a typed lambda calculus λI that internalises intensional information on how a term is computed. In the same way that the Logic...
An (n,k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical Gentzen-type systems with (n,k)-ary quantifiers are systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of an (n,k)-ary quantifier is introduced. The semantics of such systems for the case of k ∈ {0,1} are provided...
We set up differential calculi in the Cartesian-closed category CONV of convergence spaces. The central idea is to uniformly define the 3-place relation __ is a differential of __ at __ for each pair of convergence spaces X,Y in the category, where the first and second arguments are elements of Hom(X,Y) and the third argument is an element of X, in such a way as to (1) obtain the chain rule, (2) have...
We provide a model of weighted distributed systems and give a logical characterization thereof. Distributed systems are represented as weighted asynchronous cellular automata. Running over directed acyclic graphs, Mazurkiewicz traces, or (lossy) message sequence charts, they allow for modeling several communication paradigms in a unifying framework, among them probabilistic shared-variable and probabilistic...
We consider weighted o-minimal hybrid systems, which extend classical o-minimal hybrid systems with cost functions. These cost functions are “observer variables” which increase while the system evolves but do not constrain the behaviour of the system. In this paper, we prove two main results: (i) optimal o-minimal hybrid games are decidable; (ii) the model-checking of WCTL, an extension of CTL which...
Interval-based temporal logics are an important research area in computer science and artificial intelligence. In this paper we investigate decidability and expressiveness issues for Propositional Neighborhood Logics (PNLs). We begin by comparing the expressiveness of the different PNLs. Then, we focus on the most expressive one, namely, PNLπ + , and we show that it is decidable over...
In order to verify programs with pointer variables, we introduce a temporal logic LTL mem whose underlying assertion language is the quantifier-free fragment of separation logic and the temporal logic on the top of it is the standard linear-time temporal logic LTL. We analyze the complexity of various model-checking and satisfiability problems for LTL mem , considering various fragments of separation...
Deduction Modulo implements Poincarés principle by identifying deduction and computation as different paradigms and making their interaction possible. This leads to logical systems like the sequent calculus or natural deduction modulo. Even if deduction modulo is logically equivalent to first-order logic, proofs in such systems are quite different and dramatically simpler with one cost: cut elimination...
Density elimination by substitutions is introduced as a uniform method for removing applications of the Takeuti-Titani density rule from proofs in first-order hypersequent calculi. For a large class of calculi, density elimination by this method is guaranteed by known sufficient conditions for cut-elimination. Moreover, adding the density rule to any axiomatic extension of a simple first-order logic...
We prove constructively that for any propositional formula φ in Conjunctive Normal Form, we can either find a satisfying assignment of true and false to its variables, or a refutation of φ showing that it is unsatisfiable. This refutation is a resolution proof of ¬φ. From the formalization of our proof in Coq, we extract Robinson’s famous resolution algorithm as a Haskell program correct by construction...
We take the well-known intuitionistic modal logic of Fischer Servi with semantics in bi-relational Kripke frames, and give the natural extension to topological Kripke frames. Fischer Servi’s two interaction conditions relating the intuitionistic pre-order (or partial-order) with the modal accessibility relation generalise to the requirement that the relation and its inverse be lower semi-continuous...
Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this paper, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such...
We present a general algorithm scheme for model checking logics of knowledge, common knowledge and linear time, based on bisimulations to a class of structures that capture the way that agents update their knowledge. We show that the scheme leads to PSPACE implementations of model checking the logic of knowledge and linear time in several special cases: perfect recall systems with a single agent or...
LP can be seen as a logic of knowledge with justifications. Artemov’s Realization Theorem says justifications can be extracted from validities in the Hintikka-style logic of knowledge S4, where they are not explicitly present. We provide tools for reasoning about justifications directly. Among other things, we provide machinery for combining two realizations of the same formula, and for replacing...
Current symbolic techniques for the automated reasoning over undecidable hybrid automata, force one to choose between the refinement of either an overapproximation or an underapproximation of the set of reachable states. When the analysis of branching time temporal properties is considered, the literature has developed a number of abstractions techniques based on the simulation preorder, that allow...
In this paper we answer the question what implicit proof assertions in the provability logic GL can be realized by explicit proof terms. In particular we show that the fragment of GL which can be realized by generalized proof terms of GLA is exactly S4 ∩ GL and equals the fragment that can be realized by proof-terms of LP. In the final sections of this paper we establish the disjunction property for...
Hybrid systems are systems of continuous plants, subject to disturbances, interacting with sequential automata in a network. By the synthesis problem for hybrid systems we mean extracting a finite state digital controller automaton from the system equations, constraints, and cost function which define the hybrid system. This automaton senses system state, and on the basis of its state, changes state...
In this paper, we extend Moss and Parikh’s topo-logical view of knowledge. We incorporate a further modality, denoted P, into the original system. This operator describes the increase of sets. Regarding the usual logic of knowledge, P corresponds to no learning of agents. In the context of ‘topologic’, however, P represents the reverse effort operator and is related to the past therefore. It is our...
One basic activity in combinatorics is to establish combinatorial identities by so-called ‘bijective proofs,’ which amounts to constructing explicit bijections between two types of the combinatorial objects in question. The aim of this paper is to show how techniques from the formal logic world can be applied directly to such problems studied completely independently in the world of combinatorics...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.